Model checking and static analysis are well-known techniques for finding subtle flaws in software systems. However, the lack of scalability and inaccuracies in the models employed leads to false positives and are therefore detriments to their more extensive use.
Accordingly, methods which permit the more effective application of model checking and model checkers to large software systems would represent a welcome addition to the art.